ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), a:ecl(ds; da), n:. eclthrow(a; n)  ecl(ds; da) 

latex

Definitions	x:A. B(x), ecl(ds; da), t  T, eclthrow(a; n), x. t(x), x(s)
Lemmas	nat wf, decl-state wf, ma-valtype wf, bool wf, Knd wf, fpf wf, Id wf